es-decls(es;i;ds;da)
== xfpf-domain(ds).let T = ds(x) in vartype(i;x)  T
== & kfpf-domain(da).
== & let T = da(k) in e:E. loc(e) = i  isrcv(e)  kind(e) = k  valtype(e)  T 

latex

---

clarification:

es-decls(es;i;ds;da)
== xfpf-domain(ds).let T = fpf-ap(ds; IdDeq; x) in es-vartype(es; i; x)  T
== & kfpf-domain(da).
== & let T = fpf-ap(da; KindDeq; k) in 
== & e:es-E(es).
== & es-loc(es; e) = i  Id  es-isrcv(es; e)
== &  es-kind(es; e) = k  Knd
== &  es-valtype(es; e)  T 

latex

Definitions	P & Q, IdDeq, vartype(i;x), xL.P(x), fpf-domain(f), let x = a in b(x), f(x), KindDeq, x:A. B(x), E, P  Q, Id, loc(e), b, isrcv(e), P  Q, s = t, Knd, kind(e), valtype(e)
FDL editor aliases	es-decls